package controller;

import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import model.sequent.tokens.Atom;
import model.sequent.tokens.BiOperatorExpression;
import model.sequent.tokens.Expression;
import model.sequent.tokens.Sequent;
import model.sequent.tokens.SimpleOperatorExpression;

/**
 * Contains methods for reducing and evaluating a Sequent.
 * 
 * @author Karen Berntsen (s0815799)
 * @author Erik Stens (s0615374)
 */
public class SequentEvaluator {
	/**
	 * Evaluates a Sequent and returns all the counterexamples to the original proposition from which the sequent was derived.
	 * 
	 * @param sequent
	 * @return Set<Sequent> of counterexamples
	 */
	public static Set<Sequent> evaluate(Sequent sequent) {
		Set<Sequent> reducedSequentSet = reduceSequent(sequent);
		
		return evaluate(reducedSequentSet);
	}
	
	/**
	 * Evaluates a Set<Sequent> of reduced sequents and returns all the counterexamples to the original proposition from which the sequent was derived.
	 * 
	 * @param reducedSequentSet
	 * @return Set<Sequent> of counterexamples
	 */
	public static Set<Sequent> evaluate(Set<Sequent> reducedSequentSet) {
		for (Sequent sequent : reducedSequentSet) {
			if (!sequent.onlyAtoms()) {
				throw new RuntimeException("Evaluation error, one or more sequents contain expressions other than atoms!");
			}
		}
		
		Set<Sequent> counterexampleSet = new HashSet<Sequent>();
		for (Sequent sequent : reducedSequentSet) {
			if (Collections.disjoint(sequent.getTrueExpressionSet(), sequent.getFalseExpressionSet())) {
				counterexampleSet.add(sequent);
			}
		}
		
		return counterexampleSet;
	}
	
	/**
	 * Recursive function that reduces a sequent. It makes use of dynamic programming to speed up calculation by remembering previous results.
	 * 
	 * @param sequent
	 *            the sequent to reduce
	 * @return Set of Sequents representing the possible reductions of the sequent
	 */
	public static Set<Sequent> reduceSequent(Sequent sequent) {
		Map<Sequent, Set<Sequent>> knownSolutionMap = new HashMap<Sequent, Set<Sequent>>();
		Set<Sequent> sequentSet = new HashSet<Sequent>();
		
		// The reason for these elaborate loops is that the sequent can contain multiple expressions on it's 'true' and 'false' sides.
		// Because of this, all possible combinations of the results of each expression have to be made.
		
		for (Expression expression : sequent.getTrueExpressionSet()) {
			if (sequentSet.isEmpty()) {
				sequentSet = reduceExpressionRecursive(expression, true, knownSolutionMap);
			} else {
				Set<Sequent> combinedSequentSet = new HashSet<Sequent>();
				for (Sequent sequentA : sequentSet) {
					for (Sequent sequentB : reduceExpressionRecursive(expression, true, knownSolutionMap)) {
						combinedSequentSet.add(new Sequent(sequentA, sequentB));
					}
				}
				sequentSet = combinedSequentSet;
			}
		}
		
		for (Expression expression : sequent.getFalseExpressionSet()) {
			if (sequentSet.isEmpty()) {
				sequentSet = reduceExpressionRecursive(expression, false, knownSolutionMap);
			} else {
				Set<Sequent> combinedSequentSet = new HashSet<Sequent>();
				for (Sequent sequentA : sequentSet) {
					for (Sequent sequentB : reduceExpressionRecursive(expression, false, knownSolutionMap)) {
						combinedSequentSet.add(new Sequent(sequentA, sequentB));
					}
				}
				sequentSet = combinedSequentSet;
			}
		}
		
		return sequentSet;
	}
	
	/**
	 * Recursive function that reduces a single expression and then returns a Set of reduced Sequents. It makes use of dynamic programming to speed up calculation by remembering previous results.
	 * 
	 * @param expression
	 *            the expression to reduce
	 * @param side
	 *            the side of the sequent the expression is on
	 * @param knownSolutionMap
	 *            known solutions mapped to single expression sequents
	 * @return Set of Sequents representing the possible reductions of the expression
	 */
	private static Set<Sequent> reduceExpressionRecursive(Expression expression, boolean side, Map<Sequent, Set<Sequent>> knownSolutionMap) {
		Set<Sequent> sequentSet = new HashSet<Sequent>();
		Sequent sequent = side ? new Sequent(expression, null) : new Sequent(null, expression);
		
		if (expression instanceof Atom) {
			sequentSet.add(sequent);
			return sequentSet;
		}
		
		// dynamic programming
		Set<Sequent> knownSolution = knownSolutionMap.get(sequent);
		if (knownSolution != null) {
			return knownSolution;
		}
		
		if (expression instanceof SimpleOperatorExpression) {
			SimpleOperatorExpression simpleOperatorExpression = (SimpleOperatorExpression) expression;
			return reduceExpressionRecursive(simpleOperatorExpression.getExpression(), !side, knownSolutionMap);
		}
		
		if (expression instanceof BiOperatorExpression) {
			BiOperatorExpression biOperatorExpression = (BiOperatorExpression) expression;
			switch (biOperatorExpression.getOperator()) {
				case AND:
					if (side) {
						for (Sequent sequentA : reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), true, knownSolutionMap)) {
							for (Sequent sequentB : reduceExpressionRecursive(biOperatorExpression.getRightExpression(), true, knownSolutionMap)) {
								sequentSet.add(new Sequent(sequentA, sequentB));
							}
						}
					} else {
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), false, knownSolutionMap));
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getRightExpression(), false, knownSolutionMap));
					}
					knownSolutionMap.put(sequent, sequentSet);
					return sequentSet;
				case OR:
					if (side) {
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), true, knownSolutionMap));
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getRightExpression(), true, knownSolutionMap));
					} else {
						for (Sequent sequentA : reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), false, knownSolutionMap)) {
							for (Sequent sequentB : reduceExpressionRecursive(biOperatorExpression.getRightExpression(), false, knownSolutionMap)) {
								sequentSet.add(new Sequent(sequentA, sequentB));
							}
						}
					}
					knownSolutionMap.put(sequent, sequentSet);
					return sequentSet;
				case IMPLICATE:
					if (side) {
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), false, knownSolutionMap));
						sequentSet.addAll(reduceExpressionRecursive(biOperatorExpression.getRightExpression(), true, knownSolutionMap));
					} else {
						for (Sequent sequentA : reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), true, knownSolutionMap)) {
							for (Sequent sequentB : reduceExpressionRecursive(biOperatorExpression.getRightExpression(), false, knownSolutionMap)) {
								sequentSet.add(new Sequent(sequentA, sequentB));
							}
						}
					}
					knownSolutionMap.put(sequent, sequentSet);
					return sequentSet;
				case BI_IMPLICATE:
					for (Sequent sequentA : reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), true, knownSolutionMap)) {
						for (Sequent sequentB : reduceExpressionRecursive(biOperatorExpression.getRightExpression(), side, knownSolutionMap)) {
							sequentSet.add(new Sequent(sequentA, sequentB));
						}
					}
					for (Sequent sequentA : reduceExpressionRecursive(biOperatorExpression.getLeftExpression(), false, knownSolutionMap)) {
						for (Sequent sequentB : reduceExpressionRecursive(biOperatorExpression.getRightExpression(), !side, knownSolutionMap)) {
							sequentSet.add(new Sequent(sequentA, sequentB));
						}
					}
					knownSolutionMap.put(sequent, sequentSet);
					return sequentSet;
				default:
					throw new RuntimeException("Unknown operator: " + biOperatorExpression.getOperator().name() + "!");
			}
		}
		
		throw new RuntimeException("Unknown expression type: " + expression.getClass() + "!");
	}
	
	// ############################################################################################################################################################################################
	//
	// The following bit of code is the old reduction method that we wrote. Since the new one above is much clearer and even a bit faster, this method is deprecated, but we kept it here for comparison
	//
	// ############################################################################################################################################################################################
	
	/**
	 * Recursive function that returns a Set of reduced Sequents. Although the code seems impractical, it actually makes use of dynamic programming to speed up calculation by remembering previous results.
	 * 
	 * @param sequent
	 * @return Set<Sequent> of reduced Sequents
	 */
	@Deprecated
	public static Set<Sequent> reduceSequentOld(Sequent sequent) {
		return reduceSequentOldRecursive(sequent.clone());
	}
	
	@Deprecated
	private static Set<Sequent> reduceSequentOldRecursive(Sequent sequent) {
		Set<Sequent> sequentSet = new HashSet<Sequent>();
		
		Expression trueExpression = getFirstExpression(sequent.getTrueExpressionSet());
		Expression falseExpression = getFirstExpression(sequent.getFalseExpressionSet());
		
		if (trueExpression == null && falseExpression == null) {
			sequentSet.add(sequent);
			return sequentSet;
		}
		
		while (trueExpression != null || falseExpression != null) {
			if (trueExpression != null) {
				sequent.removeTrueExpression(trueExpression);
				if (trueExpression instanceof BiOperatorExpression) {
					BiOperatorExpression boe = (BiOperatorExpression) trueExpression;
					
					Set<Sequent> reducedSequentSet;
					switch (boe.getOperator()) {
						case AND:
							sequent.addTrueExpression(boe.getLeftExpression());
							sequent.addTrueExpression(boe.getRightExpression());
							sequentSet.addAll(reduceSequentOldRecursive(sequent));
							break;
						case OR:
							reducedSequentSet = reduceSequentOldRecursive(sequent);
							for (Sequent reducedSequent : reducedSequentSet) {
								Sequent reducedSequent2 = reducedSequent.clone();
								
								reducedSequent.addTrueExpression(boe.getLeftExpression());
								reducedSequent2.addTrueExpression(boe.getRightExpression());
								
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent));
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent2));
							}
							break;
						case IMPLICATE:
							reducedSequentSet = reduceSequentOldRecursive(sequent);
							for (Sequent reducedSequent : reducedSequentSet) {
								Sequent reducedSequent2 = reducedSequent.clone();
								
								reducedSequent.addFalseExpression(boe.getLeftExpression());
								reducedSequent2.addTrueExpression(boe.getRightExpression());
								
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent));
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent2));
							}
							break;
						case BI_IMPLICATE:
							reducedSequentSet = reduceSequentOldRecursive(sequent);
							for (Sequent reducedSequent : reducedSequentSet) {
								Sequent reducedSequent2 = reducedSequent.clone();
								
								reducedSequent.addTrueExpression(boe.getLeftExpression());
								reducedSequent.addTrueExpression(boe.getRightExpression());
								reducedSequent2.addFalseExpression(boe.getLeftExpression());
								reducedSequent2.addFalseExpression(boe.getRightExpression());
								
								Set<Sequent> reducedSequentSet1 = reduceSequentOldRecursive(reducedSequent);
								Set<Sequent> reducedSequentSet2 = reduceSequentOldRecursive(reducedSequent2);
								sequentSet.addAll(reducedSequentSet1);
								sequentSet.addAll(reducedSequentSet2);
							}
							break;
						default:
							throw new RuntimeException("Unknown operator: " + boe.getOperator().name() + "!");
					}
				} else if (trueExpression instanceof SimpleOperatorExpression) {
					SimpleOperatorExpression soe = (SimpleOperatorExpression) trueExpression;
					sequent.addFalseExpression(soe.getExpression());
					sequentSet.addAll(reduceSequentOldRecursive(sequent));
				} else {
					throw new RuntimeException("Invalid expression type!");
				}
				
				trueExpression = getFirstExpression(sequent.getTrueExpressionSet());
				falseExpression = getFirstExpression(sequent.getFalseExpressionSet());
			}
			
			if (falseExpression != null) {
				sequent.removeFalseExpression(falseExpression);
				if (falseExpression instanceof BiOperatorExpression) {
					BiOperatorExpression boe = (BiOperatorExpression) falseExpression;
					
					Set<Sequent> reducedSequentSet;
					switch (boe.getOperator()) {
						case AND:
							reducedSequentSet = reduceSequentOldRecursive(sequent);
							for (Sequent reducedSequent : reducedSequentSet) {
								Sequent reducedSequent2 = reducedSequent.clone();
								
								reducedSequent.addFalseExpression(boe.getLeftExpression());
								reducedSequent2.addFalseExpression(boe.getRightExpression());
								
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent));
								sequentSet.addAll(reduceSequentOldRecursive(reducedSequent2));
							}
							break;
						case OR:
							sequent.addFalseExpression(boe.getLeftExpression());
							sequent.addFalseExpression(boe.getRightExpression());
							sequentSet.addAll(reduceSequentOldRecursive(sequent));
							break;
						case IMPLICATE:
							sequent.addTrueExpression(boe.getLeftExpression());
							sequent.addFalseExpression(boe.getRightExpression());
							sequentSet.addAll(reduceSequentOldRecursive(sequent));
							break;
						case BI_IMPLICATE:
							reducedSequentSet = reduceSequentOldRecursive(sequent);
							for (Sequent reducedSequent : reducedSequentSet) {
								Sequent reducedSequent2 = reducedSequent.clone();
								
								reducedSequent.addTrueExpression(boe.getLeftExpression());
								reducedSequent.addFalseExpression(boe.getRightExpression());
								reducedSequent2.addFalseExpression(boe.getLeftExpression());
								reducedSequent2.addTrueExpression(boe.getRightExpression());
								
								Set<Sequent> reducedSequentSet1 = reduceSequentOldRecursive(reducedSequent);
								Set<Sequent> reducedSequentSet2 = reduceSequentOldRecursive(reducedSequent2);
								sequentSet.addAll(reducedSequentSet1);
								sequentSet.addAll(reducedSequentSet2);
							}
							
							break;
						default:
							throw new RuntimeException("Unknown operator: " + boe.getOperator().name() + "!");
					}
				} else if (falseExpression instanceof SimpleOperatorExpression) {
					SimpleOperatorExpression soe = (SimpleOperatorExpression) falseExpression;
					sequent.addTrueExpression(soe.getExpression());
					sequentSet.addAll(reduceSequentOldRecursive(sequent));
				} else {
					throw new RuntimeException("Invalid expression type!");
				}
				
				trueExpression = getFirstExpression(sequent.getTrueExpressionSet());
				falseExpression = getFirstExpression(sequent.getFalseExpressionSet());
			}
		}
		
		return sequentSet;
	}
	
	/**
	 * If available, returns the first expression in expressionSet that is not an Atom, otherwise
	 * 
	 * @param expressionSet
	 * @return
	 */
	@Deprecated
	private static Expression getFirstExpression(Set<Expression> expressionSet) {
		for (Expression expression : expressionSet) {
			if (!(expression instanceof Atom)) {
				return expression;
			}
		}
		return null;
	}
}